Nuprl Lemma : w-m_wf
11,40
postcript
pdf
the_w
:World,
i
:Id,
t
:
. m(
i
;
t
)
({
m
:Msg(
the_w
.M)| source(mlnk(
m
)) =
i
} List)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
w
.M
,
m(
i
;
t
)
,
t
.1
,
t
.2
,
World
Lemmas
nat
wf
,
Id
wf
,
world
wf
origin
the_w:World, i:Id, t:
. m(i;t) 
({m:Msg(the_w.M)| source(mlnk(m)) = i} List) the_w:World, i:Id, t:. m(i;t) ({m:Msg(the_w.M)| source(mlnk(m)) = i} List) x:A. B(x) T